Software testing is a basic technique to guarantee the quality of the software, and is also a process consuming most labor and resources in software development. Generally, input space of the program could often be huge or even infinite, such that the tester is unable to complete all the test cases in the limited time. Therefore, it is the most essential demand and problem to selectively generate the effective test cases in the software testing. The traditional method for selectively generating test cases mainly comprises code coverage, branch coverage and path coverage.
Test case generation methods based on the code coverage and the branch coverage has been widely used in industry. However, in comparison with random case generation method, the two methods have no statistical advantage in the detection of program errors.
Test case generation method based on the path coverage has significantly developed recently. Various tools, such as JPF-SE, Concolic and KLEE, continually arise, but all of them confront a problem of program state space explosion. The test case generation tools of the path coverage are all achieved based on symbolic execution. The symbolic execution, a program verification method advanced in the seventies of the twentieth century, is a kind of model checking method based symbolization. The symbolic execution may be widely used in symbolic debugging, test case generation and so on. The main idea of symbolic execution resides in that inputs are replaced with symbolic values and variable values in program are also expressed by symbolic expression. Finally, output values of the program may be transformed to a function with the symbolic values as inputs. The symbolic execution may abstract the program as a symbolic execution tree, wherein a sequential statement corresponds to a computational node of the tree, a branch statement corresponds to a branch node, and a loop statement is expanded to a semantically equivalent branch statement according to the number of loops. Generally speaking, one loop statement corresponds to a set of branch nodes. It could be assumed that the program only has two structures, namely sequential structure and branch structure, during the symbolic execution. The process of the symbolic execution substantially is a process of constructing a path condition. The path condition refers to a constraint condition which is necessarily satisfied by program input values for the test case to execute that path. Therefore, one path condition uniquely corresponds to an execution path. One path condition consists of a set of sub-conditions, and each condition of executed branch may serve as a sub-condition. The path condition initially is “true”. In the process of exploring the program, the path condition may be updated each time one branch statement occurs, and the condition of executed branch may be added to the path condition, wherein its formula is PC=PC^ new sub-condition. Each branch statement corresponds to two branches, namely “true” and “false”, while the symbolic execution is based on static analysis and variable has no specific value, such that it is unable to ensure the branch to be executed. Therefore, exploration will be made to the two branches (searching sequence could be defined on demand, such as an order of depth first or breadth first). That is, the conditions of two branches may serve as sub-condition to update the path condition. In such a manner, two new path conditions which correspond to two different execution paths could be achieved. Subsequently, exploration is continuously made to the two paths, respectively. The symbolic execution may achieve an overall path exploration of the program. The path conditions of all the execution paths of the program may be obtained when the program exploration is completed. Finally, all the obtained path conditions may be checked. If a path condition could not be satisfied, then this path is supposed to be an infeasible path. If a path condition could be satisfied, then this path is supposed to be feasible path. The path conditions are then passed to a constraint solver and configure out the corresponding test cases.
The symbolic execution has following two deficiencies which make it difficult to be large-scale applied. 1) The symbolic execution is a traversal algorithm based on search, which needs to traverse all branches of the program, such that although an optimization could be performed by some additional pruning conditions, the algorithm is highly complicated, i.e., O(2^n) wherein n is the number of conditional statements (inclusive of branch, loop and logistic operations) in the program. 2) The symbolic execution could not properly solve the problem of updating the test suite, and in particular, each time codes are modified, the symbolic execution tree would be re-traversed to generate anew test suite. As it could be seen from foregoing analysis, regeneration of a test suite may have a great amount of time expenditure. Moreover, software would be modified frequently; if a new test suite is generated by the symbolic execution after each modification, test efficiency will be influenced.
If a method for generating test cases is able to cover the same program behaviors as entire paths and avoid enumerating entire program paths, the efficiency of software testing would be greatly improved.